\begin{tabbing}
$\forall$${\it es}$:ES, $l$:IdLnk, $e$:E.
\\[0ex]$\exists$\=${\it e'}$:E\+
\\[0ex]($\forall$${\it e''}$:E.
\\[0ex]($\uparrow$isrcv(${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (lnk(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (${\it e''}$ c$\leq$ ${\it e'}$ \& loc(${\it e'}$) = destination($l$) $\in$ Id))
\-
\end{tabbing}